A research project aimed at the development of an automated theorem provingsystem was started in Kiev (Ukraine) in early 1960s. The mastermind of theproject, Academician V.Glushkov, baptized it "Evidence Algorithm", EA. The workon the project lasted, off and on, more than 40 years. In the framework of theproject, the Russian and English versions of the System for AutomatedDeduction, SAD, were constructed. They may be already seen as powerfultheorem-proving assistants.
展开▼
